InstLemma `assert\_of\_ff` []